(DEFPROP AUTO 
 (LAMBDA(X1)
  (PROG (N DLIST Z2 D M SAVEED SAVESTR)
	(SETQ N 1)
	(SETQ M (SETQ D 0))
   A    (SETQ M (MAX M (LENGTH (CDAR X1))))
	(SETQ D (MAX D (DEPTH (CDAR X1))))
	(SETQ Z2 (CAR X1))
	(COND
	 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
	  (SETQ DLIST (CONS N DLIST))))
	(SETQ X1 (CDR X1))
	(COND ((NULL X1) (GO B)))
	(COND ((CDR X1) (SETQ N (ADD1 N)) (GO A)))
	(SETQ M (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2))
   B    (COND ((NOT (GREATERP M 0)) (SETQ M 1)))
	(SETQ Z2 (ASSOC THEOREMNAME NEWNAME))
	(SETQ D (ADD1 D))
	(COND
	 (STRAT
	  (COND ((ZEROP ITER) (SETQ ITER 1) (COND ((NOT (EQ M 1)) (SETQ M (ADD1 M))) (T (SETQ D (ADD1 D)))))
		(T (SETQ D (ADD1 D)) (SETQ ITER 0)))))
	(COND (Z2 (SETQ SAVESTR (LIST (QUOTE AND) (QUOTE ANCESTRY) (LIST (QUOTE SUPPORT) THEOREMNAME))))
	      (T (SETQ SAVESTR (QUOTE ANCESTRY))))
	(SETQ SAVEED
	      (LIST (QUOTE OR) (LIST (QUOTE MAXDEPTH) (QUOTE (CDR C)) D) (LIST (QUOTE MAXLENGTH) (QUOTE C) M)))
	(COND ((AND EQUAL DLIST) (SETQ SAVEED (LIST (QUOTE AND) (LIST (QUOTE DEMOD) DLIST 4) SAVEED))))
	(SETQ DEBUG T)
	(COND (EQUAL (SETQ SAVESTR (CONS (QUOTE AND) (CONS SAVESTR (LIST (LIST (QUOTE PDEPTH) EQUAL 3)))))))
	(RETURN (CONS SAVESTR SAVEED)))) 
EXPR)

(DEFPROP BUILTCH1 
 (LAMBDA(X)
  (COND ((ATOM X)
	 (COND ((EQ X (QUOTE ANCESTRY)) (SETQ ANCESTRY T) NIL)
	       ((EQ X (QUOTE NONE)) NIL)
	       ((MEMQ X (QUOTE (VINE ALLPOS ALLNEG UNIT)))
		(LIST (QUOTE OR) (LIST X (QUOTE C1)) (LIST X (QUOTE C2))))
	       (T X)))
	((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE (OR (SUPPORT C2) (SUPPORT C1))))
	((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
				    (SETQ NMODEL (CADDR X))
				    (QUOTE (OR (NOT (MODEL C1)) (NOT (MODEL C2)))))
	((EQ (CAR X) (QUOTE DEFMODEL))
	 (LIST (QUOTE OR)
	       (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C1)))
	       (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C2)))))
	((EQ (CAR X) (QUOTE ANCESTRY)) (SETQ ANCESTRY T) (BUILTCH1 (CDR X)))
	((ATOM (CAR X)) (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))
	((EQ (CAAR X) (QUOTE EQUALITY)) (SETQ PDEPTH (CADAR X)) (BUILTCH1 (CDR X)))
	(T (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X)))))) 
EXPR)